The present invention relates to a technique for deriving properties of a control system, and more especially to a technique for deriving properties of a hardware system using a model of the system.
When seeking to derive the properties of a system on the basis of known transition functions of the system and all of the possible starting states, it is known to use so-called xe2x80x9cpost-imagexe2x80x9d techniques to derive the reachable states of the system. A known set of initial states is selected and the post-image of that initial set is formed to provide a first reachable set. The first reachable set is compared to the known set of reachable states and, if the known set does not comprise the first reachable set, a new set of known reachable states is formed comprising the combination of the set of reachable states and the first reachable set. If however the known set of reachable states comprises the first reachable set, the set of reachable states is determined to be an invariant of the system, and computation ceases.
Where the system model is a set of transition functions, it would be considerably more efficient to produce the so-called xe2x80x9cpre-imagexe2x80x9d of a set of states than it would be to produce the post-image. In simple terms, where each of several inputs to a system causes one of a set of outputs, a worst case for testing which input provided one particular output of interest would require all of the inputs to be applied in turn before it was possible to identify the input that gave rise to the particular output.
According to one aspect, the present invention derives transition functions for a reverse machine, i.e., a machine such that the post-image of the reverse machine will be the pre-image of the original system. The described novel technique has a large number of applications such as deriving properties of a control system using a model of the system, or deriving properties of a hardware system using a model of the system. The described novel technique may specifically be used for testing electronic circuits, testing logic circuits, including microprocessors.
According to another aspect, a method of calculating the post-image in a system includes forming a reverse model of the system, and calculating the pre-image in the reverse model, wherein the pre-image in the reverse model is equivalent to the post-image in the system. Preferably, the reverse model may be formed without knowing input states and the corresponding outputs states of the system. The formation of the reverse model may include transforming a transition function of the system into a constraint on the reverse model, and applying a parameterization of the constraint to all transitions of the reverse model.
According to yet another aspect, a method of synthesizing a reverse model of a system includes transforming a transition function of the system into a constraint on the reverse model, and applying a parameterization of the constraint to all transitions of the reverse model.
According to yet another aspect, a device for synthesizing a reverse model of a system includes a first store (a first memory), a second store (a second memory), and a processing system. The first store is constructed and arranged to store bits representative of transition functions of the system. The second store is constructed and arranged to store bits representative of an estimate of transition functions of the reverse model. The processing system includes logical device and a parameterization processor. The logical device is constructed and arranged to transform the transition functions of the system into constraints on the reverse model. The parameterization processor is arranged to apply a parameterization of the constraints to the estimate of transition functions of the reverse system to form transition functions of the reverse model.
According to yet another aspect, a device for synthesizing a reverse model of a system includes a first means for storing bits representative of transition functions of the system; a second means storing bits representative of an estimate of transition functions of the reverse model; and processing means. The processing means include a logical means for transforming the transition functions of the system into constraints on the reverse model; and a parameterization means for applying a parameterization of the constraints to the estimate of transition functions of the reverse system to form transition functions of the reverse model.
According to yet another aspect, a device for calculating the post-image in a system includes a third store (a third memory), a fourth store (a fourth memory), and a logical device. The third store is constructed and arranged to store bits representative of transition functions of a reverse model of the system. The fourth store is constructed and arranged to store bits representative of a set of states of the system. The logical device is constructed and arranged to substitute the state variables of the reverse model by the transition functions of the reverse model to provide a new set of states representing the pre-image of the reverse model, and thus provide the post-image in the system.
Preferably, the device of this aspect further comprises a first store constructed and arranged to store bits representative of transition functions of the system, and a second store constructed and arranged to store bits representative of an estimate of transition functions of the reverse model. The logical device is constructed and arranged to store transforming the transition functions of the system into constraints on the reverse models. The parameterization device is constructed and arranged to store applying a parameterization of the constraints to the estimate of transition functions of the reverse system to form transition functions of the reverse model.
Preferably, the estimate of transition functions of the reverse model comprises previous state variables of the system.
According to yet another aspect, a device for calculating the post-image in a system includes a third means for storing bits representative of transition functions of a reverse model of the system; a fourth means for storing bits representative of a set of states of the system; and logical means for substituting the state variables of the reverse model by the transition functions of the reverse model to provide a new set of states representing the pre-image of the reverse model, and thus provide the post-image in the system.